﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Collections.ObjectModel;

namespace OpSatPlan.Encoder
{
    public class OperatorEncoder
    {
        private CnfEncoder mEncoder;
        public OperatorEncoder(CnfEncoder encoder)
        {
            this.mEncoder = encoder;
        }
        public void Encode(Operator op)
        {
            ClauseTemplate clause;
            
            foreach (ReadOnlyCollection<AtomicFormula> forms in op.Preconditions)
            {
                clause = new ClauseTemplate(this.mEncoder);
                clause.Add(op, false);
                foreach (AtomicFormula form in forms)
                {
                    clause.Add(form, 0, true);
                }
                this.mEncoder.WriteClauses(clause);
            }
            foreach (ReadOnlyCollection<AtomicFormula> forms in op.AddEffects)
            {
                clause = new ClauseTemplate(this.mEncoder);
                clause.Add(op, false);
                foreach (AtomicFormula form in forms)
                {
                    clause.Add(form, 1, true);
                }
                this.mEncoder.WriteClauses(clause);
            }
            foreach (ReadOnlyCollection<AtomicFormula> forms in op.DeleteEffects)
            {
                clause = new ClauseTemplate(this.mEncoder);
                clause.Add(op, false);
                foreach (AtomicFormula form in forms)
                {
                    clause.Add(form, 1, false);
                }
                this.mEncoder.WriteClauses(clause);
            }
        }
    }
}
